_require local "../../../../basis.smi"
_require "../../../../smlformat-lib.smi"
(* _require local "../../../extensions/debug/main/Bug.smi" *)
_require local "../../../libs/list-utils/main/ListSorter.smi"
_require local "../../../data/control/main/Control.smi"

_require "../../../libs/ids/main/LocalID.smi"
_require "../../../data/symbols/main/Loc.smi"
_require "../../../data/symbols/main/RecordLabel.smi"
_require "../../../data/symbols/main/Symbol.smi"
_require "../../../data/builtin/main/BuiltinPrimitive.ppg.smi"
_require "../../../data/runtimetypes/main/RuntimeTypes.ppg.smi"
_require "../../../data/runtimetypes/main/FFIAttributes.ppg.smi"
(* _require local "../../../compilerIRs/absyn/main/AbsynTy.smi" *)
_require "../../../compilerIRs/absyn/main/InterfaceName.ppg.smi"
_require "./DummyTyID.smi"
_require "./ExistTyID.smi"
_require "./DynamicKind.ppg.smi"

structure Types =
struct
  val arrayTypId : TypID.id
  val refTypId : TypID.id

  datatype provider = datatype InterfaceName.provider
  type utvar = {symbol:Symbol.symbol, id:TvarID.id, isEq:bool, lifted:bool}
  type lambdaDepth = int

  datatype kindProperty = REIFY | BOXED | UNBOXED | EQ
  type kindPropertyList (= {})

  val propertiesOf
      : kindPropertyList -> {boxed:bool, unboxed:bool, reify:bool, eq:bool}
  val isProperties : kindProperty -> kindPropertyList -> bool
  val isSubProperties : kindPropertyList -> kindPropertyList -> bool
  val unionProperties : kindPropertyList -> kindPropertyList -> kindPropertyList
  val equalProperties : kindPropertyList -> kindPropertyList -> bool
  val emptyProperties : kindPropertyList
  val addProperties : kindProperty -> kindPropertyList -> kindPropertyList

  datatype ty =
      SINGLETONty of singletonTy
    | BACKENDty of backendTy
    | ERRORty
    | DUMMYty of DummyTyID.id * kind
    | EXISTty of ExistTyID.id * kind
    | TYVARty of tvState ref
    | BOUNDVARty of BoundTypeVarID.id
    | FUNMty of ty list * ty
    | RECORDty of ty RecordLabel.Map.map
    | CONSTRUCTty of
      {
        tyCon :
        {
          id : TypID.id,
          longsymbol : Symbol.longsymbol,
          admitsEq : bool,
          arity : int,
          conSet : (unit -> ty) option SymbolEnv.map,
          conIDSet : ConID.Set.set,
          extraArgs : ty list,
          dtyKind : dtyKind
        },
        args : ty list
      }
    | POLYty of
      {
        boundtvars : kind BoundTypeVarID.Map.map,
        constraints : constraint list,
        body : ty
      }

  and kind =
      KIND of
      {
        properties : kindPropertyList,
        tvarKind : tvarKind,
        dynamicKind : DynamicKind.dynamicKind option
      }

  and tvarKind =
      OCONSTkind of ty list
    | OPRIMkind of
      {
        instances : ty list,
        operators :
        {
          oprimId : OPrimID.id,
          longsymbol : Symbol.longsymbol,
          match : overloadMatch
        } list
      }
    | UNIV
    | REC of ty RecordLabel.Map.map

  and dtyKind =
      DTY of RuntimeTypes.property
    | OPAQUE of {opaqueRep:opaqueRep, revealKey:RevealID.id}
    | INTERFACE of opaqueRep

  and constraint =
      JOIN of {res : ty, args : ty * ty, loc:Loc.loc}

  and opaqueRep =
      TYCON of
      {
        id : TypID.id,
        longsymbol : Symbol.longsymbol,
        admitsEq : bool,
        arity : int,
        conSet : (unit -> ty) option SymbolEnv.map,
        conIDSet : ConID.Set.set,
        extraArgs : ty list,
        dtyKind : dtyKind
      }
    | TFUNDEF of {admitsEq:bool, arity:int, polyTy:ty}

  and tvState =
      TVAR of
      {
       lambdaDepth: lambdaDepth,
       id: FreeTypeVarID.id,
       kind: kind,
       utvarOpt: utvar option (* SOME: user-defined type variable *)
      }
    | SUBSTITUTED of ty

  and singletonTy =
      INSTCODEty of
      {
       oprimId : OPrimID.id,
       longsymbol : Symbol.longsymbol,
       match : overloadMatch
      }
    | INDEXty of RecordLabel.label * ty
    | TAGty of ty
    | SIZEty of ty
    | REIFYty of ty

  and backendTy =
      RECORDSIZEty of ty
    | RECORDBITMAPty of int * ty
    | RECORDBITMAPINDEXty of int * ty
    | CCONVTAGty of
      {
        tyvars : kind BoundTypeVarID.Map.map,
        haveClsEnv : bool,
        argTyList : ty list,
        retTy : ty
      }
    | FUNENTRYty of
      {
        tyvars : kind BoundTypeVarID.Map.map,
        haveClsEnv : bool,
        argTyList : ty list,
        retTy : ty
      }
    | CALLBACKENTRYty of
      {
        tyvars : kind BoundTypeVarID.Map.map,
        haveClsEnv : bool,
        argTyList : ty list,
        retTy : ty option,
        attributes : FFIAttributes.attributes
      }
    | SOME_FUNENTRYty
    | SOME_FUNWRAPPERty
    | SOME_CLOSUREENVty
    | SOME_CCONVTAGty
    | FOREIGNFUNPTRty of
      {
        argTyList : ty list,
        varArgTyList : ty list option,
        resultTy : ty option,
        attributes : FFIAttributes.attributes
      }

  and overloadMatch =
      OVERLOAD_EXVAR of
      {
        exVarInfo: {path: Symbol.longsymbol, ty: ty},
        instTyList: ty list option
      }
    | OVERLOAD_PRIM of
      {
        primInfo: {primitive: BuiltinPrimitive.primitive, ty: ty},
        instTyList: ty list option
      }
    | OVERLOAD_CASE of ty * overloadMatch TypID.Map.map

  type tvKind =
      {
        lambdaDepth: lambdaDepth,
        id: FreeTypeVarID.id,
        kind: kind,
        utvarOpt: utvar option (* SOME: user-defined type variable *)
      }

  type tyCon =
      {
        id : TypID.id,
        longsymbol : Symbol.longsymbol,
        admitsEq : bool,
        arity : int,
        conSet : (unit -> ty) option SymbolEnv.map,
        conIDSet : ConID.Set.set,
        extraArgs : ty list,
        dtyKind : dtyKind
      }

  type oprimSelector =
      {
        oprimId : OPrimID.id,
        longsymbol : Symbol.longsymbol,
        match : overloadMatch
      }

  type btvEnv = kind BoundTypeVarID.Map.map
  type varInfo = {path:Symbol.longsymbol, id:VarID.id, ty:ty, opaque:bool}
  type exVarInfo = {path:Symbol.longsymbol, ty:ty}
  type primInfo = {primitive : BuiltinPrimitive.primitive, ty : ty}
  type oprimInfo = {ty : ty, path : Symbol.longsymbol, id : OPrimID.id}
  type conInfo = {path: Symbol.longsymbol, ty: ty, id: ConID.id}
  type exnInfo = {path: Symbol.longsymbol, ty: ty, id: ExnID.id}
  type exExnInfo = {path: Symbol.longsymbol, ty: ty}

  type codeEntryTy =
      {
        tyvars : btvEnv,
        haveClsEnv : bool,
        argTyList : ty list,
        retTy : ty
      }

  type callbackEntryTy =
      {
        tyvars : btvEnv,
        haveClsEnv : bool,
        argTyList : ty list,
        retTy : ty option,
        attributes : FFIAttributes.attributes
      }

  val infiniteDepth : lambdaDepth
  val toplevelDepth : lambdaDepth
  val youngerDepth
      : {contextDepth: lambdaDepth, tyvarDepth: lambdaDepth} -> bool
  val strictlyYoungerDepth
      : {contextDepth: lambdaDepth, tyvarDepth: lambdaDepth} -> bool

  val univKind : {kind : kind, utvarOpt: utvar option}
  val emptyRecordKind : {kind : kind, utvarOpt: utvar option}
  val reifyKind : {kind : kind, utvarOpt: utvar option}
  val kindedTyvarList : tvState ref list ref
  val newTvStateRef
      : {lambdaDepth: lambdaDepth, kind : kind, utvarOpt: utvar option}
        -> tvState ref
  val newty : {kind : kind, utvarOpt: utvar option} -> ty
  val newtyWithRecordKind : ty RecordLabel.Map.map -> ty
  val newUtvar : lambdaDepth * utvar -> tvState ref
  val newtyRaw
      : {lambdaDepth: lambdaDepth, kind : kind, utvarOpt: utvar option} -> ty
  val newtyWithLambdaDepth
      : (lambdaDepth * {kind : kind, utvarOpt: utvar option}) -> ty

(*****************)
  val format_tvarKind
      : tvarKind -> SMLFormat.format
  val format_tvState
      : tvState -> SMLFormat.format
  val format_ty
      : ty -> SMLFormat.format
  val format_constraint
      : constraint -> SMLFormat.format
  val formatTyForUser
      : ['a#{env:'b, tyConName:'b * tyCon -> string}, 'b.
         'a -> ty -> SMLFormat.format]
  val format_singletonTy
      : singletonTy -> SMLFormat.format
  val format_tvKind
      : tvKind -> SMLFormat.format
  val format_dtyKind
      : dtyKind -> SMLFormat.format
  val format_oprimSelector
      : oprimSelector -> SMLFormat.format
  val format_dummyTyID : DummyTyID.id -> SMLFormat.format
(*****************)

  val format_kindPropertyList
      : kindPropertyList -> SMLFormat.format
  val format_varInfo
      : varInfo -> SMLFormat.format
  val format_exVarInfo
      : exVarInfo -> SMLFormat.format
  val format_primInfo
      : primInfo -> SMLFormat.format
  val format_oprimInfo
      : oprimInfo -> SMLFormat.format
  val format_conInfo
      : conInfo -> SMLFormat.format
  val format_codeEntryTy
      : codeEntryTy -> SMLFormat.format
  val format_callbackEntryTy
      : callbackEntryTy -> SMLFormat.format
  val format_exnInfo
      : exnInfo -> SMLFormat.format
  val format_exExnInfo
      : exExnInfo -> SMLFormat.format

  val formatWithType_varInfo
      : varInfo -> SMLFormat.format
  val formatWithType_exVarInfo
      : exVarInfo -> SMLFormat.format
  val formatWithType_primInfo
      : primInfo -> SMLFormat.format
  val format_kind
      : kind -> SMLFormat.format
  val format_btvEnv
      : btvEnv -> SMLFormat.format

end
